Library circumcircle
Require Export PointsType.
Require Import PointsETC.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition is_on_circumcircle P :=
match P with cTriple x y z ⇒
a×y×z + b×z×x + c×x×y = 0
end.
Lemma is_on_circumcircle_ok :
is_on_circumcircle pointA ∧ is_on_circumcircle pointB ∧ is_on_circumcircle pointC.
Proof.
intros.
unfold is_on_circumcircle.
simpl.
repeat split;ring.
Qed.
Lemma X_74_is_on_circumcenter :
is_on_circumcircle X_74.
Proof.
intros.
red;simpl.
unfold SA,SB,SC;repeat split;field.
Qed.
End Triangle.
Require Import PointsETC.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition is_on_circumcircle P :=
match P with cTriple x y z ⇒
a×y×z + b×z×x + c×x×y = 0
end.
Lemma is_on_circumcircle_ok :
is_on_circumcircle pointA ∧ is_on_circumcircle pointB ∧ is_on_circumcircle pointC.
Proof.
intros.
unfold is_on_circumcircle.
simpl.
repeat split;ring.
Qed.
Lemma X_74_is_on_circumcenter :
is_on_circumcircle X_74.
Proof.
intros.
red;simpl.
unfold SA,SB,SC;repeat split;field.
Qed.
End Triangle.